home *** CD-ROM | disk | FTP | other *** search
/ United Public Domain Gold 4 / United Public Domain Gold 4.iso / fredfish / ff.0316.dms / ff.0316.adf / Formulae / Formulae.scm < prev    next >
Text File  |  1990-02-06  |  11KB  |  263 lines
  1.  
  2. ;
  3. ; Formulae - Some simple and not so simple Scheme functions to handle
  4. ; sets and propositional formulaes.
  5. ; This code uses only essential procedures so it should run nice and
  6. ; easy under any Scheme.
  7. ;
  8. ; By Gauthier Groult, May 1989, with serious help from Bertrand Lecun
  9. ; - thanks Bertrand!
  10. ;
  11. ;     Gauthier Groult
  12. ;     33, Blvd Saint Denis, 92400, Courbevoie, France
  13. ;     Tel: (1) 47 89 09 54
  14. ;     EMail: groult@germinal.ibp.fr
  15. ;
  16. ; Read the joined doc file for more info.
  17. ;
  18.  
  19. ; 1. Ensembles finis.
  20. ; ~~~~~~~~~~~~~~~~~~~
  21. ;  Six fonctions permettant les manipulations de base sur les ensembles.
  22. ;  [ la fonction (inter) est ajoutee a titre illustratif, elle n'est pas
  23. ;    utilisee par la suite ]
  24. ;
  25.  
  26. (define (empty) nil)
  27.  
  28. (define (singleton x) (list x))
  29.  
  30. (define (add elem set)
  31.         (if (member elem set) set
  32.             (append (singleton elem) set)))
  33.  
  34. (define (union set1 set2)
  35.         (cond ((null? set1) set2)
  36.               ((member (car set1) set2) (union (cdr set1) set2))
  37.               (#t (cons (car set1) (union (cdr set1) set2)))))
  38.  
  39. (define (inter set1 set2)
  40.         (cond ((null? set1) ())
  41.               ((member (car set1) set2) (cons (car set1) (inter (cdr set1) set2)))
  42.               (#t (inter (cdr set1) set2))))
  43.  
  44. ; (pairs e set) retourne le produit cartesien (e) x set
  45. ;
  46. (define (pairs elem set)
  47.         (if (null? set) ()
  48.             (union (list (list elem (car set))) (pairs elem (cdr set)))))
  49.  
  50. (define (product set1 set2)
  51.         (if (null? set1) ()
  52.             (append (pairs (car set1) set2) (product (cdr set1) set2))))
  53.  
  54.  
  55. ; 2. Manipulation de formules.
  56. ; ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  57. ;  NB: toutes les fonctions definies dans cette partie sont independates de
  58. ;  l'ensemble des connecteurs utilises. On peut changer ce dernier, les
  59. ;  resultats des fonctions resteront coherents et refleteront les nouveaux
  60. ;  connecteurs.
  61. ;
  62.  
  63. ;  Definissons les connecteurs de notre espace par une liste structuree donnant
  64. ;  leur non et le nombre de leurs arguments (soit la longueur du connecteur+1).
  65. ;  [on aurait en C: struct Connector { char *name; int len; };
  66. ;                   struct Connector Connector[MAX_CONNECTORS] = { {..}, ... };]
  67. ;
  68. (define connectors '(et 3 ou 3 imp 3 equiv 3 non 2))
  69.  
  70. ;  (axioms) est la liste des quatorze axiomes du calcul propositionnel
  71. ;
  72. (define axioms
  73.         (list '(imp f (imp g f))
  74.               '(imp (imp f (imp g h)) (imp (imp f g) (imp f h)))
  75.               '(imp (et f g) f)
  76.               '(imp (et f g) g)
  77.               '(imp (imp f g) (imp (imp f h) (imp f (et g h))))
  78.               '(imp f (ou f g))
  79.               '(imp g (ou f g))
  80.               '(imp (imp f h) (imp (imp g h) (imp (ou f g) h)))
  81.               '(imp (imp f g) (imp (non g) (non f)))
  82.               '(imp f (non (non f)))
  83.               '(imp (non (non f)) f)
  84.               '(imp (equiv f g) (imp f g))
  85.               '(imp (equiv f g) (imp g f))
  86.               '(imp (imp f g) (imp (imp g f) (equiv f g)))))
  87.  
  88. ;  Quelques fontions utilitaires:
  89. ;     (connector? x) retourne le nombre d'arguments du symbole x si x est un
  90. ;                    connecteur valide, et #f s'il n'en est pas un.
  91. ;     (c1? x)        retourne #t si le symbole x est un connecteur unaire, #f sinon.
  92. ;     (c2? x)        retourne #t si le symbole x est un connecteur binaire, #f sinon.
  93. ;     (alltrue? l)   retourne #t si tous les elements de la liste l sont #t.
  94. ;     (variable? x)  retourne #t si x est un symbole non nul et n'est pas un
  95. ;                    connecteur.
  96. ;
  97. (define (connector? x)
  98.         (if (member x connectors) (cadr (member x connectors)) #f))
  99.  
  100. (define (c1? c) (if (equal? 2 (connector? c)) #t #f))
  101. (define (c2? c) (if (equal? 3 (connector? c)) #t #f))
  102.  
  103. (define (alltrue? l)
  104.         (cond ((null? l) #t) ((equal? (car l) #f) #f) (#t (alltrue? (cdr l)))))
  105.  
  106. (define (variable? x)
  107.         (not (or (null? x) (not (symbol? x)) (connector? x))))
  108.  
  109.  
  110. ;  ... et les fonctions demandees par l'enonce:
  111. ;
  112. (define (formula? f)
  113.         (or (variable? f)
  114.             (and (equal? (connector? (car f)) (length f))
  115.                  (alltrue? (map formula? (cdr f))))))
  116.  
  117. (define (vars f)
  118.         (cond ((variable? f) (singleton f))
  119.               ((c1? (car f)) (vars (cadr f)))
  120.               ((c2? (car f)) (union (vars (cadr f)) (vars (caddr f))))))
  121.  
  122. (define (subst f v g)
  123.         (if (variable? f) (if (equal? f v) g f)
  124.             (cons (car f)
  125.                   (cons (subst (cadr f) v g)
  126.                         (if (c1? (car f)) () (list (subst (caddr f) v g)))))))
  127.  
  128.  
  129. ; 3. Tables de verite.
  130. ; ~~~~~~~~~~~~~~~~~~~~
  131. ;  NB: dans cette partie les fonctions *SONT* dependantes des connecteurs
  132. ;  specifies dans la liste (connectors). Leurs resultats seront faux si cette
  133. ;  liste est alteree.
  134. ;
  135.  
  136. (define (table varset)
  137.    (if (null? varset) (singleton nil)
  138.        (letrec ((foo (lambda (x y)
  139.            (if (null? (cdr y))
  140.                (cons (append x (list (cons (car y) '(#f))))
  141.                   (list (append x (list (cons (car y) '(#t))))))
  142.                (append (foo (append x (list (cons (car y) '(#f)))) (cdr y))
  143.                   (foo (append x (list (cons (car y) '(#t)))) (cdr y)))))))
  144.        (foo () varset))))
  145.  
  146.  
  147. ;  Il faut quelques outils supplementaires pour true?, valid? et refute:
  148. ;     (xeval v a)       retourne la valeur du symbole a evalue sous l'assignation
  149. ;                       a, qui est supposee correcte.
  150. ;     (feval f a)       retourne le 'et' de l'evaluation de la formule f par toutes
  151. ;                       les assignations de la liste d'assignations a. f et a sont
  152. ;                       supposees correctes.
  153. ;     (refutes? f a)    retourne #t si l'assignation a refute la formule f, a et f
  154. ;                       etant supposees correctes.
  155. ;     (refutelist f a)  retourne la liste des assignations prises parmi la liste
  156. ;                       d'assignations a qui refutent f. a et f sont supposees
  157. ;                       etre correctement ecrites.
  158. ;
  159. (define (xeval v a) (if (member (cons v '(#t)) a) #t #f))
  160.  
  161. (define (feval f a)
  162.         (if (not (null? a)) (and (true? f (car a)) (feval f (cdr a))) #t))
  163.  
  164. (define (refutes? f a) (if (not (true? f a)) a))
  165.  
  166. (define (refutelist f a)
  167.         (if (not (null? a)) (let ((set (refutes? f (car a))))
  168.                  (if (null? set) (refutelist f (cdr a))
  169.                                  (append (list set) (refutelist f (cdr a)))))))
  170.  
  171. ; ... et les fonctions elles-memes:
  172. ;
  173. (define (true? f a)
  174.         (if (variable? f) (xeval f a)
  175.             (cond
  176.             ((eq? (car f) 'non) (not (true? (cadr f) a)))
  177.             ((eq? (car f) 'et)  (and (true? (cadr f) a) (true? (caddr f) a)))
  178.             ((eq? (car f) 'ou)  (or  (true? (cadr f) a) (true? (caddr f) a)))
  179.             ((eq? (car f) 'imp) (or  (not (true? (cadr f) a)) (true? (caddr f) a)))
  180.             ((eq? (car f) 'equiv) (eq? (true? (cadr f) a) (true? (caddr f) a))))))
  181.  
  182. (define (valid? f)
  183.         (if (formula? f) (feval f (table (vars f))) '(not a formula)))
  184.  
  185. (define (refute f)
  186.         (if (formula? f) (refutelist f (table (vars f))) '(not a formula)))
  187.  
  188.  
  189. ; 4. Connecteurs de Sheffer.
  190. ; ~~~~~~~~~~~~~~~~~~~~~~~~~~
  191. ;  NB: dans cette partie les fonctions *SONT* dependantes des connecteurs
  192. ;  specifies dans la liste (connectors). Leurs resultats seront faux si cette
  193. ;  liste est alteree.
  194. ;
  195.  
  196. ;  Trois fonctions de support pour tester si une formule est "de Sheffer":
  197. ;     (negate a)        calcule la negation de l'assignation a suppossee correcte.
  198. ;     (shefferc1? f)    retourne #t si la formule f supposee correcte verifie la
  199. ;                       premiere propriete de Sheffer.
  200. ;     (shefferc2? f)    retourne #t si la formule f supposee correcte verifie la
  201. ;                       seconde propriete de Sheffer.
  202. ;     (shefferc3? f)    retourne la liste de toutes les assignations pour lesquelles
  203. ;                       f verifie la troisieme propriete de Sheffer, s'il y en a,
  204. ;                       et #f sinon. f est supposee correcte.
  205. ;
  206. ;
  207. (define (negate a)
  208.         (append (list (list (caar a) (not (cadar a))))
  209.                 (if (null? (cdr a)) () (negate (cdr a)))))
  210.  
  211. (define (shefferc1? f) (not (true? f (product (vars f) '(#t)))))
  212.  
  213. (define (shefferc2? f) (true? f (product (vars f) '(#f))))
  214.  
  215. (define (shefferc3? f)
  216.         (letrec ((c3? (lambda (a)
  217.                 (cond ((null? a) #f)
  218.                       ((eq? (true? f (car a)) (true? f (negate (car a)))) (car a))
  219.                       (#t (c3? (cdr a))))))) (c3? (table (vars f)))))
  220.  
  221. (define (sheffer? f)
  222.         (if (not (formula? f)) '(not a formula)
  223.             (and (shefferc1? f) (shefferc2? f) (not (null? (shefferc3? f))))))
  224.  
  225. ; ... et trois fonctions de support pour la "shefferisation":
  226. ;     (s0 stroke name v)      exprime le connecteur non par le connecteur de Sheffer
  227. ;     (s1 stroke name v w)    retourne une liste semblable a s0, ou v et w sont
  228. ;                             ordonnees selon la liste retournee par shefferc3?.
  229. ;     (s2 stroke name c v w)  exprime les connecteurs et & ou par le connecteur de
  230. ;                             Sheffer. Si c=#t, et est exprime, sinon ou l'est.
  231. ;
  232. (define (s0 stroke name v)
  233.         (letrec ((dummy (lambda (x)
  234.                 (if (not (null? x)) (append (list v) (dummy (cdr x)))))))
  235.                 (cons name (dummy (vars stroke)))))
  236.  
  237. (define (s1 stroke name v w)
  238.         (letrec ((dummy (lambda (x)
  239.                 (if (not (null? x))
  240.                     (append (list (if (cadar x) v w)) (dummy (cdr x)))))))
  241.                 (cons name (dummy (shefferc3? stroke)))))
  242.  
  243. (define (s3 stroke name c v w)
  244.         (letrec ((x (shefferc3? stroke)) (sh (true? stroke x)))
  245.                  (if (equal? c sh)
  246.                      (s0 stroke name (s1 stroke name v w))
  247.                      (s1 stroke name (s0 stroke name v) (s0 stroke name w)))))
  248.  
  249. (define (shefferize stroke name f)
  250.         (letrec ((dummy (lambda (x)
  251.                 (if (variable? x) x
  252.                     (cond
  253. ((equal? (car x) 'non)   (s0 stroke name (cadr x)))
  254. ((equal? (car x) 'et)    (s3 stroke name #t (dummy (cadr x)) (dummy (caddr x))))
  255. ((equal? (car x) 'ou)    (s3 stroke name #f (dummy (cadr x)) (dummy (caddr x))))
  256. ((equal? (car x) 'imp)   (s3 stroke name #f
  257.                          (s0 stroke name (dummy (cadr x))) (dummy(caddr x))))
  258. ((equal? (car x) 'equiv) (s3 stroke name #f
  259.                          (s3 stroke name #t (dummy (cadr x)) (dummy (caddr x)))
  260.                          (s0 stroke name (s3 stroke name #f
  261.                                           (dummy (cadr x)) (dummy(caddr x)))))))))))
  262.                 (dummy f)))
  263.